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

Step	Hyp	Ref	Expression
1		dfopif 4755	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2915	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2915	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4598	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4581	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4581	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2899	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4444	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2897	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

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