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

Theorem nfop 4820
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 4800 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2923 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2923 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1902 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4643 . . . 4 𝑥{𝐴}
82, 4nfpr 4626 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4626 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2907 . . 3 𝑥
116, 9, 10nfif 4489 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2905 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2106  wnfc 2887  Vcvv 3432  c0 4256  ifcif 4459  {csn 4561  {cpr 4563  cop 4567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568
This theorem is referenced by:  nfopd  4821  moop2  5416  iunopeqop  5435  fliftfuns  7185  dfmpo  7942  qliftfuns  8593  xpf1o  8926  nfseq  13731  txcnp  22771  cnmpt1t  22816  cnmpt2t  22824  flfcnp2  23158  bnj958  32920  bnj1000  32921  bnj1446  33025  bnj1447  33026  bnj1448  33027  bnj1466  33033  bnj1467  33034  bnj1519  33045  bnj1520  33046  bnj1529  33050  nosupbnd2  33919  noinfbnd2  33934  poimirlem26  35803  nfopdALT  36985  nfaov  44671
  Copyright terms: Public domain W3C validator