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 4801	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		nfop.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfel1 2917	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
4		nfop.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfel1 2917	. . . 4 ⊢ Ⅎ𝑥 𝐵 ∈ V
6	3, 5	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)
7	2	nfsn 4639	. . . 4 ⊢ Ⅎ𝑥{𝐴}
8	2, 4	nfpr 4624	. . . 4 ⊢ Ⅎ𝑥{𝐴, 𝐵}
9	7, 8	nfpr 4624	. . 3 ⊢ Ⅎ𝑥{{𝐴}, {𝐴, 𝐵}}
10		nfcv 2901	. . 3 ⊢ Ⅎ𝑥∅
11	6, 9, 10	nfif 4485	. 2 ⊢ Ⅎ𝑥if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
12	1, 11	nfcxfr 2899	1 ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩

Syntax hints:   ∧ wa 396   ∈ wcel 2119  Ⅎwnfc 2886  Vcvv 3431  ∅c0 4261  ifcif 4454  {csn 4555  {cpr 4557  ⟨cop 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562

This theorem is referenced by:  nfopd  4821  moop2  5443  iunopeqop  5462  iunopeqopOLD  5463  fliftfuns  7258  dfmpo  8041  qliftfuns  8741  xpf1o  9067  nfseq  13964  txcnp  23603  cnmpt1t  23648  cnmpt2t  23656  flfcnp2  23990  nosupbnd2  27698  noinfbnd2  27713  nfseqs  28297  bnj958  35122  bnj1000  35123  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1466  35235  bnj1467  35236  bnj1519  35247  bnj1520  35248  bnj1529  35252  poimirlem26  38013  nfopdALT  39463  nfaov  47642