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

Theorem nfop 4347
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 4328 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2761 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2761 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1815 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4185 . . . 4 𝑥{𝐴}
82, 4nfpr 4175 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4175 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2747 . . 3 𝑥
116, 9, 10nfif 4061 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2745 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 1976  wnfc 2734  Vcvv 3169  c0 3870  ifcif 4032  {csn 4121  {cpr 4123  cop 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128
This theorem is referenced by:  nfopd  4348  moop2  4882  fliftfuns  6439  dfmpt2  7128  qliftfuns  7695  xpf1o  7981  nfseq  12625  txcnp  21172  cnmpt1t  21217  cnmpt2t  21225  flfcnp2  21560  bnj958  30067  bnj1000  30068  bnj1446  30170  bnj1447  30171  bnj1448  30172  bnj1466  30178  bnj1467  30179  bnj1519  30190  bnj1520  30191  bnj1529  30195  poimirlem26  32405  nfopdALT  33076  nfaov  39710  iunopeqop  40128
  Copyright terms: Public domain W3C validator