Theorem nfop 4833

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 4814	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2916	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2916	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1901	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4652	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4637	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4637	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2899	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4498	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2897	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Ⅎwnfc 2884  Vcvv 3430  ∅c0 4274  ifcif 4467  {csn 4568  {cpr 4570  ⟨cop 4574

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  nfopd  4834  moop2  5451  iunopeqop  5470  fliftfuns  7263  dfmpo  8046  qliftfuns  8745  xpf1o  9071  nfseq  13967  txcnp  23598  cnmpt1t  23643  cnmpt2t  23651  flfcnp2  23985  nosupbnd2  27697  noinfbnd2  27712  nfseqs  28296  bnj958  35101  bnj1000  35102  bnj1446  35206  bnj1447  35207  bnj1448  35208  bnj1466  35214  bnj1467  35215  bnj1519  35226  bnj1520  35227  bnj1529  35231  poimirlem26  37984  nfopdALT  39434  nfaov  47642