Theorem nfop 4890

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 4871	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2920	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2920	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1903	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4712	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4695	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4695	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2904	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4559	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2902	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 397   ∈ wcel 2107  Ⅎwnfc 2884  Vcvv 3475  ∅c0 4323  ifcif 4529  {csn 4629  {cpr 4631  ⟨cop 4635

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 2704

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 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  nfopd  4891  moop2  5503  iunopeqop  5522  fliftfuns  7311  dfmpo  8088  qliftfuns  8798  xpf1o  9139  nfseq  13976  txcnp  23124  cnmpt1t  23169  cnmpt2t  23177  flfcnp2  23511  nosupbnd2  27219  noinfbnd2  27234  bnj958  33951  bnj1000  33952  bnj1446  34056  bnj1447  34057  bnj1448  34058  bnj1466  34064  bnj1467  34065  bnj1519  34076  bnj1520  34077  bnj1529  34081  poimirlem26  36514  nfopdALT  37841  nfaov  45887