Theorem ralrn 7083

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6896	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6944	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2743	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3084	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5385	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  Vcvv 3464  ran crn 5660   Fn wfn 6531  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  ralrnmptw  7089  ralrnmpt  7091  cbvfo  7287  isoselem  7339  indexfi  9377  ordtypelem9  9545  ordtypelem10  9546  wemapwe  9716  numacn  10068  acndom  10070  rpnnen1lem3  13000  fsequb2  13999  limsuple  15499  limsupval2  15501  climsup  15691  ruclem11  16263  ruclem12  16264  prmreclem6  16946  imasaddfnlem  17547  imasvscafn  17556  cycsubgcl  19194  ghmrn  19217  ghmnsgima  19228  pgpssslw  19600  gexex  19839  dprdfcntz  20003  znf1o  21517  frlmlbs  21762  lindfrn  21786  ptcnplem  23564  kqt0lem  23679  isr0  23680  regr1lem2  23683  uzrest  23840  tmdgsum2  24039  imasf1oxmet  24319  imasf1omet  24320  bndth  24913  evth  24914  ovolficcss  25427  ovollb2lem  25446  ovolunlem1  25455  ovoliunlem1  25460  ovoliunlem2  25461  ovoliun2  25464  ovolscalem1  25471  ovolicc1  25474  voliunlem2  25509  voliunlem3  25510  ioombl1lem4  25519  uniioovol  25537  uniioombllem2  25541  uniioombllem3  25543  uniioombllem6  25546  volsup2  25563  vitalilem3  25568  mbfsup  25622  mbfinf  25623  mbflimsup  25624  itg1ge0  25644  itg1mulc  25662  itg1climres  25672  mbfi1fseqlem4  25676  itg2seq  25700  itg2monolem1  25708  itg2mono  25711  itg2i1fseq2  25714  itg2gt0  25718  itg2cnlem1  25719  itg2cn  25721  limciun  25852  plycpn  26254  hmopidmchi  32137  hmopidmpji  32138  rge0scvg  33985  mclsax  35596  mblfinlem2  37687  ismtyhmeolem  37833  nacsfix  42702  fnwe2lem2  43042  gneispace  44125  climinf  45602  liminfval2  45764