MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfop Structured version   Visualization version   GIF version

Theorem nfop 4449
Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
Hypotheses
Ref Expression
nfop.1 𝑥𝐴
nfop.2 𝑥𝐵
Assertion
Ref Expression
nfop 𝑥𝐴, 𝐵

Proof of Theorem nfop
StepHypRef Expression
1 dfopif 4430 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2808 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2808 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1868 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4274 . . . 4 𝑥{𝐴}
82, 4nfpr 4264 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4264 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2793 . . 3 𝑥
116, 9, 10nfif 4148 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2791 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2030  wnfc 2780  Vcvv 3231  c0 3948  ifcif 4119  {csn 4210  {cpr 4212  cop 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217
This theorem is referenced by:  nfopd  4450  moop2  4995  iunopeqop  5010  fliftfuns  6604  dfmpt2  7312  qliftfuns  7877  xpf1o  8163  nfseq  12851  txcnp  21471  cnmpt1t  21516  cnmpt2t  21524  flfcnp2  21858  bnj958  31136  bnj1000  31137  bnj1446  31239  bnj1447  31240  bnj1448  31241  bnj1466  31247  bnj1467  31248  bnj1519  31259  bnj1520  31260  bnj1529  31264  nosupbnd2  31987  poimirlem26  33565  nfopdALT  34576  nfaov  41580
  Copyright terms: Public domain W3C validator