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

Theorem nfop 4575
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 4556 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2922 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2922 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1998 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4398 . . . 4 𝑥{𝐴}
82, 4nfpr 4388 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4388 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2907 . . 3 𝑥
116, 9, 10nfif 4272 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2905 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 2155  wnfc 2894  Vcvv 3350  c0 4079  ifcif 4243  {csn 4334  {cpr 4336  cop 4340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341
This theorem is referenced by:  nfopd  4576  moop2  5121  iunopeqop  5142  fliftfuns  6756  dfmpt2  7469  qliftfuns  8037  xpf1o  8329  nfseq  13018  txcnp  21703  cnmpt1t  21748  cnmpt2t  21756  flfcnp2  22090  bnj958  31458  bnj1000  31459  bnj1446  31561  bnj1447  31562  bnj1448  31563  bnj1466  31569  bnj1467  31570  bnj1519  31581  bnj1520  31582  bnj1529  31586  nosupbnd2  32306  poimirlem26  33859  nfopdALT  34927  nfaov  41927
  Copyright terms: Public domain W3C validator