Theorem nfop 4849

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 4830	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2939	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2939	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4668	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4653	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4653	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2923	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4513	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2921	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2908  Vcvv 3451  ∅c0 4279  ifcif 4482  {csn 4584  {cpr 4586  ⟨cop 4590

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  nfopd  4850  moop2  5474  iunopeqop  5494  iunopeqopOLD  5495  fliftfuns  7322  dfmpo  8113  qliftfuns  8825  xpf1o  9158  nfseq  14154  txcnp  23939  cnmpt1t  23984  cnmpt2t  23992  flfcnp2  24326  nosupbnd2  28073  noinfbnd2  28088  nfseqs  28673  bnj958  35570  bnj1000  35571  bnj1446  35675  bnj1447  35676  bnj1448  35677  bnj1466  35683  bnj1467  35684  bnj1519  35695  bnj1520  35696  bnj1529  35700  poimirlem26  38564  nfopdALT  40028  nfaov  48248