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

Theorem nfop 4811
 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 4792 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2992 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2992 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1893 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4635 . . . 4 𝑥{𝐴}
82, 4nfpr 4620 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4620 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2975 . . 3 𝑥
116, 9, 10nfif 4494 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2973 1 𝑥𝐴, 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 398   ∈ wcel 2107  Ⅎwnfc 2959  Vcvv 3493  ∅c0 4289  ifcif 4465  {csn 4559  {cpr 4561  ⟨cop 4565 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566 This theorem is referenced by:  nfopd  4812  moop2  5383  iunopeqop  5402  fliftfuns  7059  dfmpo  7789  qliftfuns  8376  xpf1o  8671  nfseq  13371  txcnp  22220  cnmpt1t  22265  cnmpt2t  22273  flfcnp2  22607  bnj958  32200  bnj1000  32201  bnj1446  32305  bnj1447  32306  bnj1448  32307  bnj1466  32313  bnj1467  32314  bnj1519  32325  bnj1520  32326  bnj1529  32330  nosupbnd2  33204  poimirlem26  34905  nfopdALT  36094  nfaov  43363
 Copyright terms: Public domain W3C validator