Theorem nfop 4851

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 4839	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2941	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2941	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1933	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4667	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4652	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4652	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2925	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4515	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2923	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  Ⅎwnfc 2910  Vcvv 3453  ∅c0 4280  ifcif 4484  {csn 4587  {cpr 4589  ⟨cop 4837

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838

This theorem is used by:  nfopd  4852  moop2  5477  iunopeqop  5497  iunopeqopOLD  5498  fliftfuns  7329  dfmpo  8123  qliftfuns  8836  xpf1o  9169  nfseq  14164  txcnp  23951  cnmpt1t  23996  cnmpt2t  24004  flfcnp2  24338  nosupbnd2  28085  noinfbnd2  28100  nfseqs  28685  bnj958  35623  bnj1000  35624  bnj1446  35728  bnj1447  35729  bnj1448  35730  bnj1466  35736  bnj1467  35737  bnj1519  35748  bnj1520  35749  bnj1529  35753  poimirlem26  38704  nfopdALT  40168  nfaov  48388