Theorem nfop 4854

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 4842	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2942	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2942	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1934	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4669	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4654	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4654	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2926	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4516	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2924	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2147  Ⅎwnfc 2911  Vcvv 3454  ∅c0 4281  ifcif 4485  {csn 4588  {cpr 4590  ⟨cop 4840

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  nfopd  4855  moop2  5481  iunopeqop  5501  iunopeqopOLD  5502  fliftfuns  7353  dfmpo  8150  qliftfuns  8863  xpf1o  9196  nfseq  14194  txcnp  23994  cnmpt1t  24039  cnmpt2t  24047  flfcnp2  24381  nosupbnd2  28130  noinfbnd2  28145  nfseqs  28730  bnj958  35681  bnj1000  35682  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1466  35794  bnj1467  35795  bnj1519  35806  bnj1520  35807  bnj1529  35811  poimirlem26  38832  nfopdALT  40294  nfaov  48522