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 2938	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2938	. . . 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 2922	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4513	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2920	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2907  Vcvv 3450  ∅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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  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  5479  iunopeqop  5498  iunopeqopOLD  5499  fliftfuns  7316  dfmpo  8100  qliftfuns  8807  xpf1o  9140  nfseq  14078  txcnp  23849  cnmpt1t  23894  cnmpt2t  23902  flfcnp2  24236  nosupbnd2  27955  noinfbnd2  27970  nfseqs  28555  bnj958  35452  bnj1000  35453  bnj1446  35557  bnj1447  35558  bnj1448  35559  bnj1466  35565  bnj1467  35566  bnj1519  35577  bnj1520  35578  bnj1529  35582  poimirlem26  38398  nfopdALT  39847  nfaov  48070