Theorem nfop 4820

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 4800	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2923	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2923	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1902	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4643	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4626	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4626	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2907	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4489	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2905	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 396   ∈ wcel 2106  Ⅎwnfc 2887  Vcvv 3432  ∅c0 4256  ifcif 4459  {csn 4561  {cpr 4563  ⟨cop 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  nfopd  4821  moop2  5416  iunopeqop  5435  fliftfuns  7185  dfmpo  7942  qliftfuns  8593  xpf1o  8926  nfseq  13731  txcnp  22771  cnmpt1t  22816  cnmpt2t  22824  flfcnp2  23158  bnj958  32920  bnj1000  32921  bnj1446  33025  bnj1447  33026  bnj1448  33027  bnj1466  33033  bnj1467  33034  bnj1519  33045  bnj1520  33046  bnj1529  33050  nosupbnd2  33919  noinfbnd2  33934  poimirlem26  35803  nfopdALT  36985  nfaov  44671