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

Theorem nfop 4851
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 4832 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 nfop.1 . . . . 5 𝑥𝐴
32nfel1 2924 . . . 4 𝑥 𝐴 ∈ V
4 nfop.2 . . . . 5 𝑥𝐵
54nfel1 2924 . . . 4 𝑥 𝐵 ∈ V
63, 5nfan 1903 . . 3 𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
72nfsn 4673 . . . 4 𝑥{𝐴}
82, 4nfpr 4656 . . . 4 𝑥{𝐴, 𝐵}
97, 8nfpr 4656 . . 3 𝑥{{𝐴}, {𝐴, 𝐵}}
10 nfcv 2908 . . 3 𝑥
116, 9, 10nfif 4521 . 2 𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
121, 11nfcxfr 2906 1 𝑥𝐴, 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  wnfc 2888  Vcvv 3448  c0 4287  ifcif 4491  {csn 4591  {cpr 4593  cop 4597
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598
This theorem is referenced by:  nfopd  4852  moop2  5464  iunopeqop  5483  fliftfuns  7264  dfmpo  8039  qliftfuns  8750  xpf1o  9090  nfseq  13923  txcnp  22987  cnmpt1t  23032  cnmpt2t  23040  flfcnp2  23374  nosupbnd2  27080  noinfbnd2  27095  bnj958  33592  bnj1000  33593  bnj1446  33697  bnj1447  33698  bnj1448  33699  bnj1466  33705  bnj1467  33706  bnj1519  33717  bnj1520  33718  bnj1529  33722  poimirlem26  36133  nfopdALT  37462  nfaov  45485
  Copyright terms: Public domain W3C validator