Theorem nfop 4856

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 4837	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2909	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2909	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1899	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4674	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4659	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4659	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2892	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4522	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2890	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Ⅎwnfc 2877  Vcvv 3450  ∅c0 4299  ifcif 4491  {csn 4592  {cpr 4594  ⟨cop 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  nfopd  4857  moop2  5465  iunopeqop  5484  fliftfuns  7292  dfmpo  8084  qliftfuns  8780  xpf1o  9109  nfseq  13983  txcnp  23514  cnmpt1t  23559  cnmpt2t  23567  flfcnp2  23901  nosupbnd2  27635  noinfbnd2  27650  nfseqs  28188  bnj958  34937  bnj1000  34938  bnj1446  35042  bnj1447  35043  bnj1448  35044  bnj1466  35050  bnj1467  35051  bnj1519  35062  bnj1520  35063  bnj1529  35067  poimirlem26  37647  nfopdALT  38971  nfaov  47184