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

Theorem nfop 4777
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 4755 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2915 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2915 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1906 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4598 . . . 4 𝑥{𝐴}
82, 4nfpr 4581 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4581 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2899 . . 3 𝑥
116, 9, 10nfif 4444 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2897 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 399  wcel 2114  wnfc 2879  Vcvv 3398  c0 4211  ifcif 4414  {csn 4516  {cpr 4518  cop 4522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3400  df-dif 3846  df-un 3848  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523
This theorem is referenced by:  nfopd  4778  moop2  5359  iunopeqop  5378  fliftfuns  7080  dfmpo  7823  qliftfuns  8415  xpf1o  8729  nfseq  13470  txcnp  22371  cnmpt1t  22416  cnmpt2t  22424  flfcnp2  22758  bnj958  32491  bnj1000  32492  bnj1446  32596  bnj1447  32597  bnj1448  32598  bnj1466  32604  bnj1467  32605  bnj1519  32616  bnj1520  32617  bnj1529  32621  nosupbnd2  33562  noinfbnd2  33577  poimirlem26  35446  nfopdALT  36628  nfaov  44224
  Copyright terms: Public domain W3C validator