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 2943	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2943	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4675	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4660	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4660	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2927	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4520	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2925	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  Ⅎwnfc 2912  Vcvv 3457  ∅c0 4286  ifcif 4489  {csn 4591  {cpr 4593  ⟨cop 4597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  nfopd  4857  moop2  5487  iunopeqop  5506  iunopeqopOLD  5507  fliftfuns  7321  dfmpo  8103  qliftfuns  8808  xpf1o  9134  nfseq  14067  txcnp  23830  cnmpt1t  23875  cnmpt2t  23883  flfcnp2  24217  nosupbnd2  27933  noinfbnd2  27948  nfseqs  28533  bnj958  35395  bnj1000  35396  bnj1446  35500  bnj1447  35501  bnj1448  35502  bnj1466  35508  bnj1467  35509  bnj1519  35520  bnj1520  35521  bnj1529  35525  poimirlem26  38356  nfopdALT  39805  nfaov  47976