Theorem nfop 4781

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 4760	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2971	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2971	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1900	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4603	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4588	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4588	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2955	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4454	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2953	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 399   ∈ wcel 2111  Ⅎwnfc 2936  Vcvv 3441  ∅c0 4243  ifcif 4425  {csn 4525  {cpr 4527  ⟨cop 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532

This theorem is referenced by:  nfopd  4782  moop2  5357  iunopeqop  5376  fliftfuns  7046  dfmpo  7780  qliftfuns  8367  xpf1o  8663  nfseq  13374  txcnp  22225  cnmpt1t  22270  cnmpt2t  22278  flfcnp2  22612  bnj958  32322  bnj1000  32323  bnj1446  32427  bnj1447  32428  bnj1448  32429  bnj1466  32435  bnj1467  32436  bnj1519  32447  bnj1520  32448  bnj1529  32452  nosupbnd2  33329  poimirlem26  35083  nfopdALT  36267  nfaov  43735